YES(?,O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).

Strict Trs:
  { q(s(x), y) -> p(s(x), 0(), s(0()), y)
  , p(s(x), y, z, u) -> p(x, s(y), s(s(z)), u)
  , p(0(), s(x), y, z) -> q(x, add(x, z))
  , add(s(x), y) -> s(add(x, y))
  , add(0(), x) -> x }
Obligation:
  runtime complexity
Answer:
  YES(?,O(n^2))

The following argument positions are usable:
  Uargs(s) = {1}, Uargs(q) = {2}, Uargs(p) = {4}, Uargs(add) = {2}
TcT has computed following constructor-restricted polynomial
interpretation.
            [s](x1) = 2 + x1                         
                                                     
        [q](x1, x2) = 1 + x1 + x1^2 + x2             
                                                     
              [0]() = 0                              
                                                     
[p](x1, x2, x3, x4) = x1 + 2*x1*x2 + x1^2 + x2^2 + x4
                                                     
      [add](x1, x2) = 1 + 2*x1 + x2                  
                                                     

This order satisfies following ordering constraints

          [q(s(x), y)] = 7 + 5*x + x^2 + y                    
                       > 6 + 5*x + x^2 + y                    
                       = [p(s(x), 0(), s(0()), y)]            
                                                              
    [p(s(x), y, z, u)] = 6 + 5*x + 4*y + 2*x*y + x^2 + y^2 + u
                       > 5*x + 2*x*y + x^2 + 4 + 4*y + y^2 + u
                       = [p(x, s(y), s(s(z)), u)]             
                                                              
  [p(0(), s(x), y, z)] = 4 + 4*x + x^2 + z                    
                       > 2 + 3*x + x^2 + z                    
                       = [q(x, add(x, z))]                    
                                                              
        [add(s(x), y)] = 5 + 2*x + y                          
                       > 3 + 2*x + y                          
                       = [s(add(x, y))]                       
                                                              
         [add(0(), x)] = 1 + x                                
                       > x                                    
                       = [x]                                  
                                                              

Hurray, we answered YES(?,O(n^2))